\begin{problema}{procesarRespuestaT}{t: Trivia, u: Usuario, r: Texto}{SMS}
	\requiere[perteneceAParticipantes]{u \in participantes(t)}
	\requiere[perteneceAKeywords]{damePalabras(r)_0 \in keywords (t)}
	\medskip
	\modifica{t}
	\medskip
	\asegura{procesarRespuestaAux(t,pre(t),u,r,result)}
\end{problema} 

\begin{aux}{procesarRespuestaAux}{t,pret: Trivia, u: Usuario, r: Texto, result:SMS}{Bool}{\\ 
	nroDestino(result) == u\\
	\ylogico loDemasNoCambiaT(t,pret) \\
	\ylogico losDemasMismosPuntajes(t,pret,u) \\
	\ylogico losDemasMismasPreguntas(t,pret,u) \\
	\ylogico envioDeGanador(t,pret,u,result) \\
	\ylogico esUltimaCorrecta(t,pret,u,r,result) \\
	\ylogico esUltimaIncorrecta(t,pret,u,r,result)\\
	\ylogico respuestaEsCorrecta(t,pret,u,r,result)\\
	\ylogico respuestaEsIncorrecta(t,pret,u,r,result) 
}
\end{aux}

\medskip

\begin{aux}{envioDeGanador}{t,pret: Trivia, u: Usuario, result: SMS}{Bool}{\\
	(u \in ganadores(pret)) \implica \\ (ganadores(pret) == ganadores(t)  \ylogico  
	puntajeAcumulado(pret,u)==puntajeAcumulado(t,u) \ylogico \\
	texto(result)==\!''Gracias\ por\ seguir\ pagando\ pero \ el\ juego\ termino.'')
}
\end{aux}

\medskip

\begin{aux}{esUltimaCorrecta}{t,pret: Trivia, u: Usuario, r: Texto, result: SMS}{Bool}{\\
	(u \not\in ganadores(pret) \ylogico ultima(pret,u) \ylogico esCorrecta(pret,u,r))  \implica \\
	(ganadores(pret) \masmas [u]==ganadores(t) \ylogico verificarPuntaje(t,pret,u) \ylogico \\
	texto(result)==\!''Has\ respondido\ todas\ las\ preguntas.'' \masmas tusPuntos(t,u))
}
\end{aux}

\medskip

\begin{aux}{esUltimaIncorrecta}{t,pret: Trivia, u: Usuario, r: Texto, result: SMS}{Bool}{\\
	(u \not\in ganadores(pret) \ \ylogico ultima(pret,u) \ylogico \neg esCorrecta(pret,u,r))  \implica \\ 
	(ganadores(pret) \masmas [u]==ganadores(t) \ylogico puntajeAcumulado(t,u)==puntajeAcumulado(pret,u) \ylogico \\
	texto(result)==\ \!''Has\ respondido\ todas\ las\ preguntas.''\masmas tusPuntos(t,u))
}
\end{aux}

\medskip

\begin{aux}{respuestaEsCorrecta}{t,pret: Trivia, u: Usuario, r: Texto, result: SMS}{Bool}{\\
	(u \not\in ganadores(t) \ylogico \neg ultima(pret , u)  \ylogico  esCorrecta(pret,u,r)) \implica \\ 
	(ganadores(pret) == ganadores(t) \ylogico verificarPuntaje(t,pret,u) \ylogico verificarProximaPregunta(t,pret,u) \ylogico \\
	(texto(result)\ == \ \!''Bien!''\masmas tusPuntos(t,u) \masmas texto(ProxPregunta(t,u)))) 
}
\end{aux}

\medskip

\begin{aux}{respuestaEsIncorrecta}{t,pret: Trivia, u: Usuario, r: Texto, result: SMS}{Bool}{\\
	(u \not\in ganadores(t) \ylogico \neg ultima(pret , u)  \ylogico  \neg esCorrecta(pret,u,r)) \implica \\ 
	(ganadores(pret) == ganadores(t) \ylogico puntajeAcumulado(t,u)==puntajeAcumulado(pret,u) \ylogico \\
	verificarProximaPregunta(t,pret,u) \ylogico texto(result)\ == \ \!''Mal!''\masmas tusPuntos(t,u) \masmas texto(proxPregunta(t,u)))
}
\end{aux}

\medskip

\begin{aux}{tusPuntos}{t: Trivia, u: Usuario}{String}{
	''Tenes\ '' \masmas 
	intToString(puntajeAcumulado(t,u)) \masmas ''\ pts.\ ''
}
\end{aux}

\medskip

\begin{aux}{esCorrecta}{t: Trivia, u: Usuario, r: Texto}{Bool}{\\
	damePalabras(r)_{(0\ldots\longitud{damePalabras(r)})} == damePalabras(rtaCorrecta(proxPregunta(t,u)))
}
\end{aux}

\medskip

\begin{aux}{ultima}{t: Trivia, u: Usuario}{Bool}{\\
	\longitud{dameIndiceProxPregunta(t,u)} \not= 0
	\ylogico (cab(dameIndiceProxPregunta(t,u)) + 1) == \longitud{preguntas(t)}
}
\end{aux}

\medskip

\begin{aux}{dameIndiceProxPregunta}{t: Trivia, u: Usuario}{[Int]}{\\
	\comp{i}{i\selec [0..\longitud{preguntas(t)}), proxPregunta(t,u) ==
	preguntas(t)_i } 
	}
\end{aux}

\medskip

\begin{aux}{verificarProximaPregunta}{t,pret:Trivia, u:Usuario}{Bool}{\\
	\longitud{dameIndiceProxPregunta(t,u)} \not= 0 \ylogico\\
	 cab(dameIndiceProxPregunta(pret,u)) + 1 == cab(dameIndiceProxPregunta(t,u))
}
\end{aux}

\medskip

\begin{aux}{verificarPuntaje}{t,pret:Trivia, u:Usuario}{Bool}{\\
	puntajeAcum(pret,u) + puntaje(proxPregunta(pret,u)) == puntajeAcum(t,u)
}
\end{aux}


